Inference at * 
Iof proof for Lemma nth tl is fseg:


  T:Type, L1, L2:(T List). fseg(T;L1;L2)  (n:{0..(||L2||+1)}. (L1 = nth_tl(n;L2))) 

latex

 by ((((Unfold `fseg` 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term)))) 
CollapseTHEN (ExRepD)) 

latex

C1: 

C1: 1. T : Type
C1: 2. L1 : T List
C1: 3. L2 : T List
C1: 4. L : T List
C1: 5. L2 = (L @ L1)
C1:   n:{0..(||L2||+1)}. (L1 = nth_tl(n;L2))
C2: 

C2: 1. T : Type
C2: 2. L1 : T List
C2: 3. L2 : T List
C2: 4. n : {0..(||L2||+1)}
C2: 5. L1 = nth_tl(n;L2)
C2:   L:T List. (L2 = (L @ L1))
C.

Definitions	fseg(T;L1;L2), P  Q, P & Q, P  Q, P  Q, , {x:A| B(x)} , , x:A. B(x), x:AB(x), t  T, {i..j}, n+m, ||as||, #$n, nth_tl(n;as), s = t, as @ bs, type List, Type, x:A. B(x), x:A  B(x)
Lemmas	nth tl wf, int seg wf, length wf1, append wf